Nuprl Lemma : pairwise-nil
0,22
postcript
pdf
P
:Top. (
x
,
y
nil.
P
(
x
,
y
))
True
latex
Definitions
P
Q
,
P
Q
,
True
,
Top
,
(
x
,
y
L
.
P
(
x
;
y
))
,
x
(
s1
,
s2
)
,
i
j
<
k
,
A
B
,
P
&
Q
,
A
,
False
,
P
Q
,
t
T
,
{
i
..
j
}
,
x
:
A
.
B
(
x
)
Lemmas
int
seg
wf
,
top
wf
,
true
wf
origin
P:Top. (x,y
nil.P(x,y)) 
True P:Top. (x,ynil.P(x,y)) True Q
Qx,yL.P(x;y))
j < kB
A Q T
}x:A. B(x)